package flowlogic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;

import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Z3Exception;

import ast.ChannelConstant;
import ast.Constant;
import ast.Label;
import ast.Network;
import ast.NewConstN;
import ast.NewConstP;
import ast.ParallelNetwork;
import ast.ParallelProcess;
import ast.Process;
import ast.ProcessAtSite;
import ast.Term;

public class NetworkJudgement extends FLJudgement {
	
	private Network network;
	private HashMap<String, HashSet<Term>> kappa;
	private BoolExpr varphi;
	private PsiNode psi;
	
	public NetworkJudgement(
			Network n, 
			HashMap<String, HashSet<Term>> rho, 
			HashMap<String, HashSet<Term>> kappa,
			BoolExpr varphi
			)
	{
		network = n;
		setRho(rho);
		this.kappa = kappa;
		this.varphi = varphi;
		psi = new PsiNode();
	}
	
	public PsiNode getPsi()
	{
		return psi;
	}
	
	public String toString()
	{
		String res = "rho, kappa |- " + "(" + varphi + ")" + 
						network.toString(0) + " : " + psi;
		return res;
	}

	public ArrayList<DischargeResult> discharge()  
	{
		ArrayList<DischargeResult> resList = new ArrayList<DischargeResult>();
		
		if (network instanceof NewConstN) {
			
			Constant c = ((NewConstN) network).getConstant();
			if (c instanceof ChannelConstant) {
				Label lb = ((ChannelConstant) c).getLabel();
				LabelJudgement lbjgt = new LabelJudgement(lb);
				resList.add(new Inclusion(lbjgt.getPsi(), psi, true));
			}
			
			NetworkJudgement njdgt = new NetworkJudgement(
					((NewConstN) network).getNetwork(), getRho(), kappa, varphi);
			resList.add(njdgt);
			resList.add(new Inclusion(njdgt.getPsi(), psi, true));
			
		} else if (network instanceof ParallelNetwork) {
			
			NetworkJudgement njdgt = null;
			for (Network curNet : ((ParallelNetwork) network).getComponentNetworks()) {
				njdgt = new NetworkJudgement(curNet, getRho(), kappa, varphi);
				resList.add(njdgt);
				resList.add(new Inclusion(njdgt.getPsi(), psi, true));
			}
			
		} else if (network instanceof ProcessAtSite) {
			
			// use the version of constructor that takes a given "psi"
			resList.add(
					new ProcessJudgement(((ProcessAtSite) network).getProcess(), 
										getRho(), kappa, varphi, psi)
			);
			
		}
		
		return resList;
	}
	
}
